Nuprl Lemma : world-rename_wf 0,22
w:World, rx, ra:(IdId), rainv:(Id(Id+Unit)), rt:(IdId), rtinv:(Id(Id+Unit)).
inv-rel(Id;Id;ra;rainv)
 inv-rel(Id;Id;rt;rtinv)
 world-rename(rx;ra;rt;rainv;rtinv;w)  World 
latex

Definitionst  T, x:A. B(x)
Lemmasnat wf, Msg wf, lsrc wf, mlnk wf, w-automaton wf, top wf

origin